chore: adaptations to nightly-2024-03-11 #11314
Conversation
kim-em
commented
Mar 12, 2024
•
kim-em
commented
![github-actions[bot]](https://avatars.githubusercontent.com/in/15368?s=60&v=4){kind=small}
Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
…nity/mathlib4 into bump/nightly-2024-03-11
…nity/mathlib4 into bump/nightly-2024-03-11
Backported from #11314.
|
!bench |
| rw [← add_assoc] | ||
| -- Adaptation note: nightly-2024-03-11 | ||
| -- I'm not sure why the `erw` is now needed here. It looks like it should work. | ||
| erw [hc] |
There was a problem hiding this comment.
It looks like it has a problem unfolding c itself so tries to unify Nat.rec and HSub.hsub
There was a problem hiding this comment.
Do you want to expand the comment?
There was a problem hiding this comment.
It looks like at diamond at this transparency between instHAdd and AddSemigroup.toAdd
| | [], l' => l' | ||
| | l, [] => l | ||
| | a :: l, b :: l' => if a ≼ b then a :: merge l (b :: l') else b :: merge (a :: l) l' | ||
| | a :: l, b :: l' => if a ≼ b then a :: merge' l (b :: l') else b :: merge' (a :: l) l' | ||
| termination_by l₁ l₂ => length l₁ + length l₂ | ||
| #align list.merge List.merge |
There was a problem hiding this comment.
Should List.merge being renamed be documented? (And should we mention leanprover-community/batteries#579 ?) I see there's an adaptation underway by @fgdorais
(And should the #align to List.merge' here? Or keep it with List.merge since that seems to be where the adaptation is going?)
There was a problem hiding this comment.
Oh, oops, let's undo this in this PR. My mistake.
There was a problem hiding this comment.
Okay, I've revert this change, and instead incorporated the change from #11347
|
Here are the benchmark results for commit 09b5587.Found no runs to compare against. |
|
I've looked through all the changes, and everything (except for questions about |
Something terrible happened in injective resolutions |
It's still on overall improvement on instructions (very minor) and wall-clock, so we don't need to hold on this, right? |
|
Don’t hold. It is probably something silly. Looking now |
|
Added comment with label |
|
🤦♂️ |
